COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	auxili[f81,jmc]		Proofs of program properties using auxiliary entities
C00005 ENDMK
C⊗;
auxili[f81,jmc]		Proofs of program properties using auxiliary entities


	The elementary proofs of properties of LISP programs use only the
variables and quantities occurring in the programs.  It seems that this
isn't the general case.  In general proofs and statements of correctness
should involve abstract entities for which no machine representation is
given.

	A first idea about this occurs when we discuss sort programs.
We can introduce the bag of a list as an abstract entity, and the
result of sorting a list has the same bag and is sorted.  Perhaps
unfortunately, bags aren't really necessary for this problem; it
seems simpler to make to with

	mult(x,u) ← if n u then 0
		else if x = a u then 1 + mult(x,d u)
		else mult(x,d u).

	We can easily prove

	∀x u v. mult(x,u*v) = mult(x,u)+mult(x,v),

but we really want

	∀x u v. mult(x,merge(u,v)) = mult(x,u) + mult(x,v)

where

	merge(u,v) ← if nu then v
		else if n v then u
		ele if π(u,v) then a u . merge(d u,v)
		else a v . merge(u, d v),

and  π(u,v)  is any predicate whatsoever, but is taken as  a u ≤ a v in
the usual sorting case.  In fact  π  could depend on completely extraneous
information such as the phase of the moon.
  There are possibilities for treating the
general case using ambiguous functions defining relations,etc.  The
proof of this last formula wants to be a rank induction with

	rank(u,v) = length u + length v.